the_es:event_system{i:l}, e,e':es-E(the_es). decidable((e = e')) 

latex

Definitions

decidable(P), x:AB(x), x:A. B(x), b, s = t, P  Q, x:A  B(x), x:A. B(x), divides(b; a), assoced(a; b), set_leq(p; a; b), set_lt(p; a; b), grp_lt(g; a; b), A c B, f(a), x f y, l_all(L; T; x.P(x)), l_exists(L; T; x.P(x)), qle(r; s), qless(r; s), q-rel(r; x), p-outcome(p), (x  l), l_disjoint(T; l1; l2), event_system{i:l}, es-E(es), t  T, e = e', Type, prop{i:l}, P  Q, P  Q, P  Q, strong-subtype(A; B), left + right, P  Q, False, A, , a < b, A  B, atom, int_seg(i; j), , quotient(A; x,y.B(x;y)), set_car(p), grp_car(g), rng_car(r), Unit, , , atom{$n:n}, rationals, dstype(TypeNames; d; a), Id, IdLnk, Knd, MaName

Lemmas

event system wf, decidable functionality, assert-es-eq-E, es-E wf, es-eq-E wf, assert wf, decidable wf, decidable assert